0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 9 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 14.1 s)
↳12 BOUNDS(1, n^2)
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
minus(x, 0) → x
minus(s(x), s(y)) → s(minus(x, y))
gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, transform(y))), s(min(x, y)))
transform(x) → s(s(x))
transform(cons(x, y)) → cons(cons(x, x), x)
transform(cons(x, y)) → y
transform(s(x)) → s(s(transform(x)))
cons(x, y) → y
cons(x, cons(y, s(z))) → cons(y, x)
cons(cons(x, z), s(y)) → transform(x)
max(x, 0) → x
max(0, y) → y
gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, transform(y))), s(min(x, y)))
min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
minus(s(x), s(y)) → s(minus(x, y))
transform(x) → s(s(x))
cons(x, y) → y
max(s(x), s(y)) → s(max(x, y))
minus(x, 0) → x
transform(s(x)) → s(s(transform(x)))
max(x, 0) → x [1]
max(0, y) → y [1]
gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, transform(y))), s(min(x, y))) [1]
min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
minus(s(x), s(y)) → s(minus(x, y)) [1]
transform(x) → s(s(x)) [1]
cons(x, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
minus(x, 0) → x [1]
transform(s(x)) → s(s(transform(x))) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, transform(y))), s(min(x, y))) [1]
min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
minus(s(x), s(y)) → s(minus(x, y)) [1]
transform(x) → s(s(x)) [1]
cons(x, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
minus(x, 0) → x [1]
transform(s(x)) → s(s(transform(x))) [1]
| max :: 0:s → 0:s → 0:s 0 :: 0:s gcd :: 0:s → 0:s → gcd s :: 0:s → 0:s minus :: 0:s → 0:s → 0:s min :: 0:s → 0:s → 0:s transform :: 0:s → 0:s cons :: a → cons → cons |
gcd(v0, v1) → null_gcd [0]
minus(v0, v1) → null_minus [0]
max(v0, v1) → null_max [0]
min(v0, v1) → null_min [0]
null_gcd, null_minus, null_max, null_min, const, const1
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
null_gcd => 0
null_minus => 0
null_max => 0
null_min => 0
const => 0
const1 => 0
cons(z, z') -{ 1 }→ y :|: x >= 0, y >= 0, z = x, z' = y
gcd(z, z') -{ 1 }→ gcd(minus(max(x, y), min(x, transform(y))), 1 + min(x, y)) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gcd(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
max(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
max(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
max(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
max(z, z') -{ 1 }→ 1 + max(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
min(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0
min(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
min(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
min(z, z') -{ 1 }→ 1 + min(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
minus(z, z') -{ 1 }→ 1 + minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
transform(z) -{ 1 }→ 1 + (1 + x) :|: x >= 0, z = x
transform(z) -{ 1 }→ 1 + (1 + transform(x)) :|: x >= 0, z = 1 + x
| eq(start(V, V1),0,[max(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[min(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[transform(V, Out)],[V >= 0]). eq(start(V, V1),0,[cons(V, V1, Out)],[V >= 0,V1 >= 0]). eq(max(V, V1, Out),1,[],[Out = V2,V2 >= 0,V = V2,V1 = 0]). eq(max(V, V1, Out),1,[],[Out = V3,V3 >= 0,V = 0,V1 = V3]). eq(gcd(V, V1, Out),1,[max(V4, V5, Ret00),transform(V5, Ret011),min(V4, Ret011, Ret01),minus(Ret00, Ret01, Ret0),min(V4, V5, Ret11),gcd(Ret0, 1 + Ret11, Ret)],[Out = Ret,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(min(V, V1, Out),1,[],[Out = 0,V6 >= 0,V = V6,V1 = 0]). eq(min(V, V1, Out),1,[],[Out = 0,V7 >= 0,V = 0,V1 = V7]). eq(min(V, V1, Out),1,[min(V8, V9, Ret1)],[Out = 1 + Ret1,V1 = 1 + V9,V8 >= 0,V9 >= 0,V = 1 + V8]). eq(minus(V, V1, Out),1,[minus(V10, V11, Ret12)],[Out = 1 + Ret12,V1 = 1 + V11,V10 >= 0,V11 >= 0,V = 1 + V10]). eq(transform(V, Out),1,[],[Out = 2 + V12,V12 >= 0,V = V12]). eq(cons(V, V1, Out),1,[],[Out = V13,V14 >= 0,V13 >= 0,V = V14,V1 = V13]). eq(max(V, V1, Out),1,[max(V15, V16, Ret13)],[Out = 1 + Ret13,V1 = 1 + V16,V15 >= 0,V16 >= 0,V = 1 + V15]). eq(minus(V, V1, Out),1,[],[Out = V17,V17 >= 0,V = V17,V1 = 0]). eq(transform(V, Out),1,[transform(V18, Ret111)],[Out = 2 + Ret111,V18 >= 0,V = 1 + V18]). eq(gcd(V, V1, Out),0,[],[Out = 0,V19 >= 0,V20 >= 0,V = V19,V1 = V20]). eq(minus(V, V1, Out),0,[],[Out = 0,V21 >= 0,V22 >= 0,V = V21,V1 = V22]). eq(max(V, V1, Out),0,[],[Out = 0,V23 >= 0,V24 >= 0,V = V23,V1 = V24]). eq(min(V, V1, Out),0,[],[Out = 0,V25 >= 0,V26 >= 0,V = V25,V1 = V26]). input_output_vars(max(V,V1,Out),[V,V1],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(min(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(transform(V,Out),[V],[Out]). input_output_vars(cons(V,V1,Out),[V,V1],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [cons/3]
1. recursive : [max/3]
2. recursive : [min/3]
3. recursive : [minus/3]
4. recursive : [transform/2]
5. recursive : [gcd/3]
6. non_recursive : [start/2]
#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is partially evaluated into max/3
2. SCC is partially evaluated into min/3
3. SCC is partially evaluated into minus/3
4. SCC is partially evaluated into transform/2
5. SCC is partially evaluated into gcd/3
6. SCC is partially evaluated into start/2
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations max/3
* CE 11 is refined into CE [23]
* CE 8 is refined into CE [24]
* CE 9 is refined into CE [25]
* CE 10 is refined into CE [26]
### Cost equations --> "Loop" of max/3
* CEs [26] --> Loop 16
* CEs [23] --> Loop 17
* CEs [24] --> Loop 18
* CEs [25] --> Loop 19
### Ranking functions of CR max(V,V1,Out)
* RF of phase [16]: [V,V1]
#### Partial ranking functions of CR max(V,V1,Out)
* Partial RF of phase [16]:
- RF of loop [16:1]:
V
V1
### Specialization of cost equations min/3
* CE 14 is refined into CE [27]
* CE 15 is refined into CE [28]
* CE 17 is refined into CE [29]
* CE 16 is refined into CE [30]
### Cost equations --> "Loop" of min/3
* CEs [30] --> Loop 20
* CEs [27] --> Loop 21
* CEs [28,29] --> Loop 22
### Ranking functions of CR min(V,V1,Out)
* RF of phase [20]: [V,V1]
#### Partial ranking functions of CR min(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1
### Specialization of cost equations minus/3
* CE 20 is refined into CE [31]
* CE 19 is refined into CE [32]
* CE 18 is refined into CE [33]
### Cost equations --> "Loop" of minus/3
* CEs [33] --> Loop 23
* CEs [31] --> Loop 24
* CEs [32] --> Loop 25
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [23]: [V,V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [23]:
- RF of loop [23:1]:
V
V1
### Specialization of cost equations transform/2
* CE 22 is refined into CE [34]
* CE 21 is refined into CE [35]
### Cost equations --> "Loop" of transform/2
* CEs [35] --> Loop 26
* CEs [34] --> Loop 27
### Ranking functions of CR transform(V,Out)
* RF of phase [27]: [V]
#### Partial ranking functions of CR transform(V,Out)
* Partial RF of phase [27]:
- RF of loop [27:1]:
V
### Specialization of cost equations gcd/3
* CE 13 is refined into CE [36]
* CE 12 is refined into CE [37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117]
### Cost equations --> "Loop" of gcd/3
* CEs [67,77] --> Loop 28
* CEs [87,97,99,105,107,109,115,117] --> Loop 29
* CEs [79,85,89,95] --> Loop 30
* CEs [59,65,69,75] --> Loop 31
* CEs [86,96,98,104,106,108,114,116] --> Loop 32
* CEs [66,76] --> Loop 33
* CEs [78,84,88,94] --> Loop 34
* CEs [58,64,68,74] --> Loop 35
* CEs [61,63,71,73] --> Loop 36
* CEs [47,49,51,53,55,57,81,83,91,93,101,103,111,113] --> Loop 37
* CEs [45] --> Loop 38
* CEs [41,44] --> Loop 39
* CEs [42,43] --> Loop 40
* CEs [37,39] --> Loop 41
* CEs [38,40,46,48,50,52,54,56,60,62,70,72,80,82,90,92,100,102,110,112] --> Loop 42
* CEs [36] --> Loop 43
### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [28,29,30,31]: [V+V1-3]
* RF of phase [38,39,41]: [V+V1-1]
#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [28,29,30,31]:
- RF of loop [28:1,29:1,31:1]:
V-1 depends on loops [30:1]
- RF of loop [29:1,30:1]:
V+V1-3
* Partial RF of phase [38,39,41]:
- RF of loop [38:1]:
V-1 depends on loops [41:1]
- RF of loop [39:1]:
V depends on loops [41:1]
- RF of loop [41:1]:
V+V1-1
### Specialization of cost equations start/2
* CE 2 is refined into CE [118,119,120,121,122,123]
* CE 3 is refined into CE [124]
* CE 4 is refined into CE [125,126]
* CE 5 is refined into CE [127,128,129,130]
* CE 6 is refined into CE [131,132]
* CE 7 is refined into CE [133]
### Cost equations --> "Loop" of start/2
* CEs [119,127] --> Loop 44
* CEs [118,120,121,122,123,124,125,126,128,129,130,131,132,133] --> Loop 45
### Ranking functions of CR start(V,V1)
#### Partial ranking functions of CR start(V,V1)
Computing Bounds
=====================================
#### Cost of chains of max(V,V1,Out):
* Chain [[16],19]: 1*it(16)+1
Such that:it(16) =< V
with precondition: [V1=Out,V>=1,V1>=V]
* Chain [[16],18]: 1*it(16)+1
Such that:it(16) =< V1
with precondition: [V=Out,V1>=1,V>=V1]
* Chain [[16],17]: 1*it(16)+0
Such that:it(16) =< Out
with precondition: [Out>=1,V>=Out,V1>=Out]
* Chain [19]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [18]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [17]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of min(V,V1,Out):
* Chain [[20],22]: 1*it(20)+1
Such that:it(20) =< Out
with precondition: [Out>=1,V>=Out,V1>=Out]
* Chain [[20],21]: 1*it(20)+1
Such that:it(20) =< Out
with precondition: [V1=Out,V1>=1,V>=V1]
* Chain [22]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [21]: 1
with precondition: [V1=0,Out=0,V>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[23],25]: 1*it(23)+1
Such that:it(23) =< V1
with precondition: [V=Out,V1>=1,V>=V1]
* Chain [[23],24]: 1*it(23)+0
Such that:it(23) =< Out
with precondition: [Out>=1,V>=Out,V1>=Out]
* Chain [25]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [24]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of transform(V,Out):
* Chain [[27],26]: 1*it(27)+1
Such that:it(27) =< -V+Out
with precondition: [Out>=V+3,2*V+2>=Out]
* Chain [26]: 1
with precondition: [V+2=Out,V>=0]
#### Cost of chains of gcd(V,V1,Out):
* Chain [[38,39,41],43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+0
Such that:aux(16) =< 2
s(17) =< 2*V+3*V1
aux(34) =< V
aux(35) =< V+V1
aux(36) =< 2*V
aux(37) =< 3*V
aux(38) =< V1
it(38) =< aux(35)
it(39) =< aux(35)
it(41) =< aux(35)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(34)
it(39) =< aux(38)+aux(34)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(35)
s(14) =< s(16)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[38,39,41],42,43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+5
Such that:aux(42) =< 1
aux(44) =< 2
aux(45) =< V
aux(46) =< V+V1
aux(47) =< 2*V
aux(48) =< 2*V+3*V1
aux(49) =< 3*V
aux(50) =< V1
s(17) =< aux(48)
s(26) =< aux(42)
s(18) =< aux(44)
it(38) =< aux(46)
it(39) =< aux(46)
it(41) =< aux(46)
aux(7) =< aux(50)*3
aux(12) =< aux(50)*2
it(38) =< aux(50)+aux(45)
it(39) =< aux(50)+aux(45)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(46)
s(14) =< s(16)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[38,39,41],40,43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+9
Such that:aux(16) =< 2
s(17) =< 2*V+3*V1
aux(51) =< V
aux(52) =< V+V1
aux(53) =< 2*V
aux(54) =< 3*V
aux(55) =< V1
it(38) =< aux(52)
it(39) =< aux(52)
it(41) =< aux(52)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(51)
it(39) =< aux(55)+aux(51)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(52)
s(14) =< s(16)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[28,29,30,31],[38,39,41],43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+0
Such that:aux(16) =< 2
aux(110) =< 2*V+3*V1
aux(36) =< 6*V+6*V1
s(17) =< 9*V+9*V1
aux(109) =< V1
aux(111) =< V
aux(112) =< V+V1
aux(113) =< 3*V+3*V1
it(38) =< aux(112)
it(39) =< aux(112)
it(41) =< aux(112)
aux(7) =< aux(113)*3
aux(12) =< aux(113)*2
it(38) =< aux(113)+aux(113)
it(39) =< aux(113)+aux(113)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(113)
s(16) =< aux(7)+aux(113)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(112)
s(14) =< s(16)
it(28) =< aux(112)
it(30) =< aux(112)
it(28) =< aux(113)
it(30) =< aux(113)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(112)
aux(93) =< aux(112)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(111)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(112)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[28,29,30,31],[38,39,41],42,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+5
Such that:aux(42) =< 1
aux(44) =< 2
aux(110) =< 2*V+3*V1
aux(47) =< 6*V+6*V1
aux(109) =< V1
aux(114) =< V
aux(115) =< V+V1
aux(116) =< 3*V+3*V1
aux(117) =< 9*V+9*V1
s(17) =< aux(117)
s(26) =< aux(42)
s(18) =< aux(44)
it(38) =< aux(115)
it(39) =< aux(115)
it(41) =< aux(115)
aux(7) =< aux(116)*3
aux(12) =< aux(116)*2
it(38) =< aux(116)+aux(116)
it(39) =< aux(116)+aux(116)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(117)
s(16) =< aux(7)+aux(117)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(115)
s(14) =< s(16)
it(28) =< aux(115)
it(30) =< aux(115)
it(28) =< aux(117)
it(30) =< aux(117)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(115)
aux(93) =< aux(115)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(114)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(115)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[28,29,30,31],[38,39,41],40,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+9
Such that:aux(16) =< 2
aux(110) =< 2*V+3*V1
aux(53) =< 6*V+6*V1
s(17) =< 9*V+9*V1
aux(109) =< V1
aux(118) =< V
aux(119) =< V+V1
aux(120) =< 3*V+3*V1
it(38) =< aux(119)
it(39) =< aux(119)
it(41) =< aux(119)
aux(7) =< aux(120)*3
aux(12) =< aux(120)*2
it(38) =< aux(120)+aux(120)
it(39) =< aux(120)+aux(120)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(120)
s(16) =< aux(7)+aux(120)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(119)
s(14) =< s(16)
it(28) =< aux(119)
it(30) =< aux(119)
it(28) =< aux(120)
it(30) =< aux(120)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(119)
aux(93) =< aux(119)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(118)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(119)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[28,29,30,31],43]: 16*it(28)+6*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+0
Such that:aux(121) =< V
aux(122) =< V+V1
aux(123) =< V1
it(28) =< aux(122)
it(30) =< aux(122)
aux(87) =< aux(123)
aux(85) =< aux(123)+1
aux(90) =< aux(122)
aux(93) =< aux(122)-1
aux(86) =< aux(123)*2
it(28) =< aux(123)+aux(121)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(123)
s(195) =< it(28)*aux(122)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[28,29,30,31],42,43]: 16*it(28)+6*it(30)+30*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+5
Such that:aux(109) =< V1
aux(110) =< V1+1
aux(124) =< V
aux(125) =< V+V1
aux(126) =< V+V1+1
s(18) =< aux(126)
s(26) =< aux(125)
it(28) =< aux(125)
it(30) =< aux(125)
it(28) =< aux(126)
it(30) =< aux(126)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(125)
aux(93) =< aux(125)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(124)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(125)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[28,29,30,31],37,43]: 16*it(28)+54*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+7*s(231)+5
Such that:aux(131) =< V+V1+1
aux(134) =< V
aux(135) =< V+V1
aux(136) =< V1
it(30) =< aux(135)
s(231) =< aux(131)
it(28) =< aux(135)
aux(87) =< aux(136)
aux(85) =< aux(136)+1
aux(90) =< aux(135)
aux(93) =< aux(135)-1
aux(86) =< aux(136)*2
it(28) =< aux(136)+aux(134)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(136)
s(195) =< it(28)*aux(135)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],36,43]: 16*it(28)+6*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+12*s(278)+6*s(283)+5
Such that:aux(109) =< V1
aux(110) =< V1+1
aux(142) =< V
aux(143) =< V+V1
aux(144) =< V+V1+1
s(278) =< aux(143)
s(283) =< aux(144)
it(28) =< aux(143)
it(30) =< aux(143)
it(28) =< aux(144)
it(30) =< aux(144)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(143)
aux(93) =< aux(143)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(142)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(143)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],35,[38,39,41],43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+8*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+5*s(299)+6
Such that:aux(38) =< 1
aux(16) =< 2
aux(106) =< V+V1
aux(148) =< 2*V+2*V1+3
aux(37) =< 6*V+6*V1
aux(109) =< V1
aux(110) =< 2*V1
aux(150) =< V
aux(151) =< 2*V+2*V1
aux(152) =< 2*V+2*V1+1
s(17) =< aux(152)
it(38) =< aux(151)
it(39) =< aux(151)
it(41) =< aux(151)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(151)
it(39) =< aux(38)+aux(151)
it(39) =< aux(12)+aux(151)
s(15) =< aux(12)+aux(151)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(151)
s(14) =< s(16)
s(299) =< aux(148)
it(28) =< aux(106)
it(30) =< aux(106)
it(28) =< aux(152)
it(30) =< aux(152)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(106)
aux(93) =< aux(106)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(150)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(106)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],35,[38,39,41],42,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+9*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(296)+5*s(299)+11
Such that:aux(153) =< 1
aux(44) =< 2
aux(148) =< V+V1+1
aux(48) =< 2*V+2*V1+1
aux(49) =< 6*V+6*V1
aux(109) =< V1
aux(110) =< 2*V1
aux(155) =< V
aux(156) =< V+V1
aux(157) =< 2*V+2*V1
s(17) =< aux(48)
s(26) =< aux(153)
s(18) =< aux(44)
it(38) =< aux(157)
it(39) =< aux(157)
it(41) =< aux(157)
aux(7) =< aux(153)*3
aux(12) =< aux(153)*2
it(38) =< aux(153)+aux(157)
it(39) =< aux(153)+aux(157)
it(39) =< aux(12)+aux(157)
s(15) =< aux(12)+aux(157)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(157)
s(14) =< s(16)
s(296) =< aux(156)
s(299) =< aux(148)
it(28) =< aux(156)
it(30) =< aux(156)
it(28) =< aux(157)
it(30) =< aux(157)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(156)
aux(93) =< aux(156)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(155)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(156)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]
* Chain [[28,29,30,31],35,[38,39,41],40,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+8*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+5*s(299)+15
Such that:aux(55) =< 1
aux(16) =< 2
aux(106) =< V+V1
aux(148) =< 2*V+2*V1+3
aux(54) =< 6*V+6*V1
aux(109) =< V1
aux(110) =< 2*V1
aux(159) =< V
aux(160) =< 2*V+2*V1
aux(161) =< 2*V+2*V1+1
s(17) =< aux(161)
it(38) =< aux(160)
it(39) =< aux(160)
it(41) =< aux(160)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(160)
it(39) =< aux(55)+aux(160)
it(39) =< aux(12)+aux(160)
s(15) =< aux(12)+aux(160)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(160)
s(14) =< s(16)
s(299) =< aux(148)
it(28) =< aux(106)
it(30) =< aux(106)
it(28) =< aux(161)
it(30) =< aux(161)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(106)
aux(93) =< aux(106)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(159)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(106)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]
* Chain [[28,29,30,31],35,43]: 16*it(28)+6*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(296)+5*s(299)+3*s(306)+6
Such that:aux(148) =< V1+1
aux(162) =< V
aux(163) =< V+V1
aux(164) =< V1
aux(165) =< 2*V1
s(296) =< aux(164)
s(299) =< aux(148)
s(306) =< aux(165)
it(28) =< aux(163)
it(30) =< aux(163)
aux(79) =< aux(164)
aux(79) =< aux(165)
aux(87) =< aux(164)
aux(85) =< aux(164)+1
aux(90) =< aux(163)
aux(93) =< aux(163)-1
aux(86) =< aux(164)*2
it(28) =< aux(79)+aux(162)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(164)
s(195) =< it(28)*aux(163)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],35,42,43]: 16*it(28)+6*it(30)+10*s(18)+25*s(20)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(296)+3*s(306)+11
Such that:aux(42) =< 1
aux(43) =< 2
aux(146) =< 2*V+2*V1
aux(109) =< V1
aux(110) =< 2*V1
aux(166) =< V
aux(167) =< V+V1
aux(168) =< V+V1+1
s(20) =< aux(168)
s(26) =< aux(42)
s(18) =< aux(43)
s(296) =< aux(167)
s(306) =< aux(146)
it(28) =< aux(167)
it(30) =< aux(167)
it(28) =< aux(168)
it(30) =< aux(168)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(167)
aux(93) =< aux(167)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(166)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(167)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],35,40,43]: 16*it(28)+6*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(296)+5*s(299)+3*s(306)+15
Such that:aux(148) =< V1+1
aux(169) =< V
aux(170) =< V+V1
aux(171) =< V1
aux(172) =< 2*V1
s(296) =< aux(171)
s(299) =< aux(148)
s(306) =< aux(172)
it(28) =< aux(170)
it(30) =< aux(170)
aux(79) =< aux(171)
aux(79) =< aux(172)
aux(87) =< aux(171)
aux(85) =< aux(171)+1
aux(90) =< aux(170)
aux(93) =< aux(170)-1
aux(86) =< aux(171)*2
it(28) =< aux(79)+aux(169)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(171)
s(195) =< it(28)*aux(170)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],34,[38,39,41],43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+10*s(308)+2*s(314)+6
Such that:aux(38) =< 1
aux(16) =< 2
aux(176) =< V+V1+1
aux(36) =< 2*V+2*V1
s(17) =< 2*V+2*V1+1
aux(109) =< V1
aux(110) =< 3*V1
aux(178) =< V
aux(179) =< V+V1
aux(180) =< 3*V+3*V1
it(38) =< aux(179)
it(39) =< aux(179)
it(41) =< aux(179)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(179)
it(39) =< aux(38)+aux(179)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(180)
s(16) =< aux(7)+aux(180)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(179)
s(14) =< s(16)
s(308) =< aux(180)
s(314) =< aux(176)
it(28) =< aux(179)
it(30) =< aux(179)
it(28) =< aux(180)
it(30) =< aux(180)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(179)
aux(93) =< aux(179)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(178)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(179)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],34,[38,39,41],42,43]: 16*it(28)+22*it(30)+5*it(38)+12*it(39)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+2*s(314)+11
Such that:aux(181) =< 1
aux(44) =< 2
aux(176) =< V+V1+1
aux(47) =< 2*V+2*V1
aux(48) =< 2*V+2*V1+1
aux(49) =< 3*V+3*V1
aux(109) =< V1
aux(110) =< 3*V1
aux(183) =< V
aux(184) =< V+V1
s(17) =< aux(48)
s(26) =< aux(181)
s(18) =< aux(44)
it(38) =< aux(184)
it(39) =< aux(184)
it(30) =< aux(184)
aux(7) =< aux(181)*3
aux(12) =< aux(181)*2
it(38) =< aux(181)+aux(184)
it(39) =< aux(181)+aux(184)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(184)
s(14) =< s(16)
s(314) =< aux(176)
it(28) =< aux(184)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(184)
aux(93) =< aux(184)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(183)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(184)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [[28,29,30,31],34,[38,39,41],40,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+11*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+2*s(314)+15
Such that:aux(55) =< 1
aux(16) =< 2
aux(176) =< V+V1+1
aux(53) =< 2*V+2*V1
aux(54) =< 3*V+3*V1
aux(109) =< V1
aux(110) =< 3*V1
aux(186) =< V
aux(187) =< V+V1
aux(188) =< 2*V+2*V1+1
s(17) =< aux(188)
it(38) =< aux(187)
it(39) =< aux(187)
it(41) =< aux(187)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(187)
it(39) =< aux(55)+aux(187)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(187)
s(14) =< s(16)
s(314) =< aux(176)
it(28) =< aux(187)
it(30) =< aux(187)
it(28) =< aux(188)
it(30) =< aux(188)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(187)
aux(93) =< aux(187)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(186)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(187)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [[28,29,30,31],34,43]: 16*it(28)+6*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+12*s(308)+6
Such that:aux(106) =< V+V1
aux(109) =< V1
aux(110) =< V1+1
aux(189) =< V
aux(190) =< V+V1+1
s(308) =< aux(190)
it(28) =< aux(106)
it(30) =< aux(106)
it(28) =< aux(190)
it(30) =< aux(190)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(106)
aux(93) =< aux(106)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(189)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(106)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],34,42,43]: 16*it(28)+6*it(30)+10*s(18)+20*s(20)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+12*s(308)+11
Such that:aux(42) =< 1
aux(43) =< 2
aux(109) =< V1
aux(110) =< V1+1
aux(191) =< V
aux(192) =< V+V1
aux(193) =< V+V1+1
s(20) =< aux(192)
s(26) =< aux(42)
s(18) =< aux(43)
s(308) =< aux(193)
it(28) =< aux(192)
it(30) =< aux(192)
it(28) =< aux(193)
it(30) =< aux(193)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(192)
aux(93) =< aux(192)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(191)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(192)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],34,40,43]: 16*it(28)+6*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+12*s(308)+15
Such that:aux(106) =< V+V1
aux(109) =< V1
aux(110) =< V1+1
aux(194) =< V
aux(195) =< V+V1+1
s(308) =< aux(195)
it(28) =< aux(106)
it(30) =< aux(106)
it(28) =< aux(195)
it(30) =< aux(195)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(106)
aux(93) =< aux(106)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(194)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(106)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],33,[38,39,41],43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+12*it(41)+2*s(14)+1*s(15)+3*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+1*s(325)+5
Such that:aux(38) =< 1
aux(16) =< 2
aux(36) =< 2*V+2*V1
s(325) =< 2*V+2*V1+3
aux(37) =< 3*V+3*V1
aux(200) =< V
aux(201) =< V+V1
aux(202) =< 2*V+2*V1+1
aux(203) =< V1
s(17) =< aux(202)
it(38) =< aux(201)
it(39) =< aux(201)
it(41) =< aux(201)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(201)
it(39) =< aux(38)+aux(201)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(201)
s(14) =< s(16)
it(28) =< aux(201)
it(30) =< aux(201)
it(28) =< aux(202)
it(30) =< aux(202)
aux(87) =< aux(203)
aux(85) =< aux(203)+1
aux(90) =< aux(201)
aux(93) =< aux(201)-1
aux(86) =< aux(203)*2
it(28) =< aux(203)+aux(200)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(203)
s(195) =< it(28)*aux(201)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],33,[38,39,41],42,43]: 16*it(28)+20*it(30)+5*it(38)+12*it(39)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+1*s(325)+10
Such that:aux(204) =< 1
aux(44) =< 2
s(325) =< V+V1+1
aux(47) =< 2*V+2*V1
aux(48) =< 2*V+2*V1+1
aux(49) =< 3*V+3*V1
aux(206) =< V
aux(207) =< V+V1
aux(208) =< V1
s(17) =< aux(48)
s(26) =< aux(204)
s(18) =< aux(44)
it(38) =< aux(207)
it(39) =< aux(207)
it(30) =< aux(207)
aux(7) =< aux(204)*3
aux(12) =< aux(204)*2
it(38) =< aux(204)+aux(207)
it(39) =< aux(204)+aux(207)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(207)
s(14) =< s(16)
it(28) =< aux(207)
aux(87) =< aux(208)
aux(85) =< aux(208)+1
aux(90) =< aux(207)
aux(93) =< aux(207)-1
aux(86) =< aux(208)*2
it(28) =< aux(208)+aux(206)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(208)
s(195) =< it(28)*aux(207)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]
* Chain [[28,29,30,31],33,[38,39,41],40,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+12*it(41)+2*s(14)+1*s(15)+3*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+1*s(325)+14
Such that:aux(55) =< 1
aux(16) =< 2
aux(53) =< 2*V+2*V1
s(325) =< 2*V+2*V1+3
aux(54) =< 3*V+3*V1
aux(210) =< V
aux(211) =< V+V1
aux(212) =< 2*V+2*V1+1
aux(213) =< V1
s(17) =< aux(212)
it(38) =< aux(211)
it(39) =< aux(211)
it(41) =< aux(211)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(211)
it(39) =< aux(55)+aux(211)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(211)
s(14) =< s(16)
it(28) =< aux(211)
it(30) =< aux(211)
it(28) =< aux(212)
it(30) =< aux(212)
aux(87) =< aux(213)
aux(85) =< aux(213)+1
aux(90) =< aux(211)
aux(93) =< aux(211)-1
aux(86) =< aux(213)*2
it(28) =< aux(213)+aux(210)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(213)
s(195) =< it(28)*aux(211)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]
* Chain [[28,29,30,31],33,43]: 16*it(28)+14*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+1*s(325)+5
Such that:s(325) =< V+V1+1
aux(215) =< V
aux(216) =< V+V1
aux(217) =< V1
it(30) =< aux(216)
it(28) =< aux(216)
aux(87) =< aux(217)
aux(85) =< aux(217)+1
aux(90) =< aux(216)
aux(93) =< aux(216)-1
aux(86) =< aux(217)*2
it(28) =< aux(217)+aux(215)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(217)
s(195) =< it(28)*aux(216)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],33,42,43]: 16*it(28)+34*it(30)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+1*s(325)+10
Such that:aux(42) =< 1
aux(43) =< 2
s(325) =< V+V1+1
aux(219) =< V
aux(220) =< V+V1
aux(221) =< V1
it(30) =< aux(220)
s(26) =< aux(42)
s(18) =< aux(43)
it(28) =< aux(220)
aux(87) =< aux(221)
aux(85) =< aux(221)+1
aux(90) =< aux(220)
aux(93) =< aux(220)-1
aux(86) =< aux(221)*2
it(28) =< aux(221)+aux(219)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(221)
s(195) =< it(28)*aux(220)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],33,40,43]: 16*it(28)+14*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+1*s(325)+14
Such that:s(325) =< V+V1+1
aux(223) =< V
aux(224) =< V+V1
aux(225) =< V1
it(30) =< aux(224)
it(28) =< aux(224)
aux(87) =< aux(225)
aux(85) =< aux(225)+1
aux(90) =< aux(224)
aux(93) =< aux(224)-1
aux(86) =< aux(225)*2
it(28) =< aux(225)+aux(223)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(225)
s(195) =< it(28)*aux(224)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],32,[38,39,41],43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+22*it(41)+2*s(14)+1*s(15)+11*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(334)+5
Such that:aux(38) =< 1
aux(16) =< 2
aux(232) =< V+V1+1
aux(36) =< 2*V+2*V1
aux(37) =< 3*V+3*V1
aux(109) =< V1
aux(110) =< 3*V1
aux(235) =< V
aux(236) =< V+V1
aux(237) =< 2*V+2*V1+1
s(17) =< aux(237)
it(38) =< aux(236)
it(39) =< aux(236)
it(41) =< aux(236)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(236)
it(39) =< aux(38)+aux(236)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(236)
s(14) =< s(16)
s(334) =< aux(232)
it(28) =< aux(236)
it(30) =< aux(236)
it(28) =< aux(237)
it(30) =< aux(237)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(236)
aux(93) =< aux(236)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(235)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(236)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],32,[38,39,41],42,43]: 16*it(28)+38*it(30)+5*it(38)+12*it(39)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(334)+10
Such that:aux(238) =< 1
aux(44) =< 2
aux(232) =< V+V1+1
aux(47) =< 2*V+2*V1
aux(48) =< 2*V+2*V1+1
aux(49) =< 3*V+3*V1
aux(109) =< V1
aux(110) =< 2*V1+1
aux(240) =< V
aux(241) =< V+V1
s(17) =< aux(48)
s(26) =< aux(238)
s(18) =< aux(44)
it(38) =< aux(241)
it(39) =< aux(241)
it(30) =< aux(241)
aux(7) =< aux(238)*3
aux(12) =< aux(238)*2
it(38) =< aux(238)+aux(241)
it(39) =< aux(238)+aux(241)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(241)
s(14) =< s(16)
s(334) =< aux(232)
it(28) =< aux(241)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(241)
aux(93) =< aux(241)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(240)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(241)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]
* Chain [[28,29,30,31],32,[38,39,41],40,43]: 16*it(28)+6*it(30)+5*it(38)+12*it(39)+22*it(41)+2*s(14)+1*s(15)+11*s(17)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(334)+14
Such that:aux(55) =< 1
aux(16) =< 2
aux(232) =< V+V1+1
aux(53) =< 2*V+2*V1
aux(54) =< 3*V+3*V1
aux(109) =< V1
aux(110) =< 3*V1
aux(243) =< V
aux(244) =< V+V1
aux(245) =< 2*V+2*V1+1
s(17) =< aux(245)
it(38) =< aux(244)
it(39) =< aux(244)
it(41) =< aux(244)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(244)
it(39) =< aux(55)+aux(244)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(244)
s(14) =< s(16)
s(334) =< aux(232)
it(28) =< aux(244)
it(30) =< aux(244)
it(28) =< aux(245)
it(30) =< aux(245)
aux(79) =< aux(109)
aux(79) =< aux(110)
aux(87) =< aux(109)
aux(85) =< aux(109)+1
aux(90) =< aux(244)
aux(93) =< aux(244)-1
aux(86) =< aux(109)*2
it(28) =< aux(79)+aux(243)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(109)
s(195) =< it(28)*aux(244)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]
* Chain [[28,29,30,31],32,43]: 16*it(28)+32*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(334)+5
Such that:aux(232) =< V+V1+1
aux(247) =< V
aux(248) =< V+V1
aux(249) =< V1
it(30) =< aux(248)
s(334) =< aux(232)
it(28) =< aux(248)
aux(87) =< aux(249)
aux(85) =< aux(249)+1
aux(90) =< aux(248)
aux(93) =< aux(248)-1
aux(86) =< aux(249)*2
it(28) =< aux(249)+aux(247)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(249)
s(195) =< it(28)*aux(248)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],32,42,43]: 16*it(28)+52*it(30)+10*s(18)+8*s(26)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(334)+10
Such that:aux(42) =< 1
aux(43) =< 2
aux(232) =< V+V1+1
aux(251) =< V
aux(252) =< V+V1
aux(253) =< V1
it(30) =< aux(252)
s(26) =< aux(42)
s(18) =< aux(43)
s(334) =< aux(232)
it(28) =< aux(252)
aux(87) =< aux(253)
aux(85) =< aux(253)+1
aux(90) =< aux(252)
aux(93) =< aux(252)-1
aux(86) =< aux(253)*2
it(28) =< aux(253)+aux(251)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(253)
s(195) =< it(28)*aux(252)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [[28,29,30,31],32,40,43]: 16*it(28)+32*it(30)+2*s(190)+4*s(191)+2*s(192)+18*s(193)+1*s(194)+26*s(199)+14*s(200)+9*s(202)+18*s(209)+2*s(211)+3*s(218)+4*s(334)+14
Such that:aux(232) =< V+V1+1
aux(255) =< V
aux(256) =< V+V1
aux(257) =< V1
it(30) =< aux(256)
s(334) =< aux(232)
it(28) =< aux(256)
aux(87) =< aux(257)
aux(85) =< aux(257)+1
aux(90) =< aux(256)
aux(93) =< aux(256)-1
aux(86) =< aux(257)*2
it(28) =< aux(257)+aux(255)
s(212) =< it(30)*aux(90)
s(213) =< it(30)*aux(85)
aux(103) =< it(28)*aux(87)
s(207) =< it(28)*aux(85)
s(204) =< it(28)*aux(90)
s(206) =< it(28)*aux(93)
s(197) =< it(28)*aux(86)
s(194) =< it(28)*aux(85)
s(198) =< it(28)*aux(257)
s(195) =< it(28)*aux(256)
s(219) =< aux(103)*2
s(193) =< aux(103)
s(202) =< s(207)
s(218) =< s(219)
s(209) =< s(212)
s(211) =< s(213)
s(200) =< s(206)
s(199) =< s(204)
s(190) =< s(198)
s(192) =< s(197)
s(191) =< s(195)
with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]
* Chain [43]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [42,43]: 10*s(18)+20*s(20)+8*s(26)+5
Such that:aux(41) =< V
aux(42) =< V1
aux(43) =< V1+1
s(20) =< aux(41)
s(26) =< aux(42)
s(18) =< aux(43)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [40,43]: 9
with precondition: [V1=1,Out=0,V>=1]
* Chain [37,43]: 45*s(224)+7*s(231)+3*s(263)+5
Such that:aux(130) =< V1
aux(131) =< V1+1
aux(133) =< V
s(224) =< aux(133)
s(263) =< aux(130)
s(231) =< aux(131)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [36,43]: 12*s(278)+4*s(283)+2*s(287)+5
Such that:aux(137) =< V
aux(139) =< V1+1
aux(141) =< V1
s(278) =< aux(141)
s(287) =< aux(139)
s(283) =< aux(137)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [35,[38,39,41],43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+4*s(296)+5*s(299)+3*s(306)+6
Such that:aux(38) =< 1
aux(16) =< 2
aux(36) =< 2*V
s(17) =< 2*V+1
aux(37) =< 3*V
aux(147) =< V1
aux(148) =< V1+1
aux(146) =< 2*V1
aux(149) =< V
it(38) =< aux(149)
it(39) =< aux(149)
it(41) =< aux(149)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(149)
it(39) =< aux(38)+aux(149)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(149)
s(14) =< s(16)
s(296) =< aux(147)
s(299) =< aux(148)
s(306) =< aux(146)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [35,[38,39,41],42,43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+4*s(296)+5*s(299)+3*s(306)+11
Such that:aux(44) =< 2
aux(47) =< 2*V
aux(48) =< 2*V+1
aux(49) =< 3*V
aux(147) =< V1
aux(148) =< V1+1
aux(146) =< 2*V1
aux(153) =< 1
aux(154) =< V
s(17) =< aux(48)
s(26) =< aux(153)
s(18) =< aux(44)
it(38) =< aux(154)
it(39) =< aux(154)
it(41) =< aux(154)
aux(7) =< aux(153)*3
aux(12) =< aux(153)*2
it(38) =< aux(153)+aux(154)
it(39) =< aux(153)+aux(154)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(154)
s(14) =< s(16)
s(296) =< aux(147)
s(299) =< aux(148)
s(306) =< aux(146)
with precondition: [Out=0,V>=3,V1>=2,V>=V1]
* Chain [35,[38,39,41],40,43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+4*s(296)+5*s(299)+3*s(306)+15
Such that:aux(55) =< 1
aux(16) =< 2
aux(53) =< 2*V
s(17) =< 2*V+1
aux(54) =< 3*V
aux(147) =< V1
aux(148) =< V1+1
aux(146) =< 2*V1
aux(158) =< V
it(38) =< aux(158)
it(39) =< aux(158)
it(41) =< aux(158)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(158)
it(39) =< aux(55)+aux(158)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(158)
s(14) =< s(16)
s(296) =< aux(147)
s(299) =< aux(148)
s(306) =< aux(146)
with precondition: [Out=0,V>=3,V1>=2,V>=V1]
* Chain [35,43]: 4*s(296)+5*s(299)+3*s(306)+6
Such that:aux(147) =< V1
aux(148) =< V1+1
aux(146) =< 2*V1
s(296) =< aux(147)
s(299) =< aux(148)
s(306) =< aux(146)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [35,42,43]: 10*s(18)+20*s(20)+8*s(26)+4*s(296)+5*s(299)+3*s(306)+11
Such that:aux(42) =< 1
aux(43) =< 2
aux(41) =< V
aux(147) =< V1
aux(148) =< V1+1
aux(146) =< 2*V1
s(20) =< aux(41)
s(26) =< aux(42)
s(18) =< aux(43)
s(296) =< aux(147)
s(299) =< aux(148)
s(306) =< aux(146)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [35,40,43]: 4*s(296)+5*s(299)+3*s(306)+15
Such that:aux(147) =< V1
aux(148) =< V1+1
aux(146) =< 2*V1
s(296) =< aux(147)
s(299) =< aux(148)
s(306) =< aux(146)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [34,[38,39,41],43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+10*s(308)+2*s(314)+6
Such that:aux(38) =< 1
aux(16) =< 2
aux(175) =< V
aux(176) =< V1+1
aux(36) =< 2*V1
s(17) =< 2*V1+1
aux(37) =< 3*V1
aux(177) =< V1
it(38) =< aux(177)
it(39) =< aux(177)
it(41) =< aux(177)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(177)
it(39) =< aux(38)+aux(177)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(177)
s(14) =< s(16)
s(308) =< aux(175)
s(314) =< aux(176)
with precondition: [Out=0,V>=2,V1>=V]
* Chain [34,[38,39,41],42,43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+10*s(308)+2*s(314)+11
Such that:aux(44) =< 2
aux(175) =< V
aux(176) =< V1+1
aux(47) =< 2*V1
aux(48) =< 2*V1+1
aux(49) =< 3*V1
aux(181) =< 1
aux(182) =< V1
s(17) =< aux(48)
s(26) =< aux(181)
s(18) =< aux(44)
it(38) =< aux(182)
it(39) =< aux(182)
it(41) =< aux(182)
aux(7) =< aux(181)*3
aux(12) =< aux(181)*2
it(38) =< aux(181)+aux(182)
it(39) =< aux(181)+aux(182)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(182)
s(14) =< s(16)
s(308) =< aux(175)
s(314) =< aux(176)
with precondition: [Out=0,V>=2,V1>=3,V1>=V]
* Chain [34,[38,39,41],40,43]: 5*it(38)+12*it(39)+6*it(41)+2*s(14)+1*s(15)+1*s(17)+10*s(308)+2*s(314)+15
Such that:aux(55) =< 1
aux(16) =< 2
aux(175) =< V
aux(176) =< V1+1
aux(53) =< 2*V1
s(17) =< 2*V1+1
aux(54) =< 3*V1
aux(185) =< V1
it(38) =< aux(185)
it(39) =< aux(185)
it(41) =< aux(185)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(185)
it(39) =< aux(55)+aux(185)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(185)
s(14) =< s(16)
s(308) =< aux(175)
s(314) =< aux(176)
with precondition: [Out=0,V>=2,V1>=3,V1>=V]
* Chain [34,43]: 10*s(308)+2*s(314)+6
Such that:aux(175) =< V
aux(176) =< V1+1
s(308) =< aux(175)
s(314) =< aux(176)
with precondition: [Out=0,V>=2,V1>=V]
* Chain [34,42,43]: 10*s(18)+20*s(20)+8*s(26)+10*s(308)+2*s(314)+11
Such that:aux(42) =< 1
aux(43) =< 2
aux(175) =< V
aux(41) =< V1
aux(176) =< V1+1
s(20) =< aux(41)
s(26) =< aux(42)
s(18) =< aux(43)
s(308) =< aux(175)
s(314) =< aux(176)
with precondition: [Out=0,V>=2,V1>=V]
* Chain [34,40,43]: 10*s(308)+2*s(314)+15
Such that:aux(175) =< V
aux(176) =< V1+1
s(308) =< aux(175)
s(314) =< aux(176)
with precondition: [Out=0,V>=2,V1>=V]
* Chain [33,[38,39,41],43]: 5*it(38)+12*it(39)+12*it(41)+2*s(14)+1*s(15)+1*s(17)+2*s(320)+1*s(325)+5
Such that:aux(38) =< 1
aux(16) =< 2
aux(36) =< 2*V
s(17) =< 2*V+1
aux(37) =< 3*V
aux(197) =< V1
s(325) =< V1+1
aux(199) =< V
it(38) =< aux(199)
it(39) =< aux(199)
it(41) =< aux(199)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(199)
it(39) =< aux(38)+aux(199)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(199)
s(14) =< s(16)
s(320) =< aux(197)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [33,[38,39,41],42,43]: 5*it(38)+12*it(39)+12*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+2*s(320)+1*s(325)+10
Such that:aux(44) =< 2
aux(47) =< 2*V
aux(48) =< 2*V+1
aux(49) =< 3*V
aux(197) =< V1
s(325) =< V1+1
aux(204) =< 1
aux(205) =< V
s(17) =< aux(48)
s(26) =< aux(204)
s(18) =< aux(44)
it(38) =< aux(205)
it(39) =< aux(205)
it(41) =< aux(205)
aux(7) =< aux(204)*3
aux(12) =< aux(204)*2
it(38) =< aux(204)+aux(205)
it(39) =< aux(204)+aux(205)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(205)
s(14) =< s(16)
s(320) =< aux(197)
with precondition: [Out=0,V>=3,V1>=2,V>=V1]
* Chain [33,[38,39,41],40,43]: 5*it(38)+12*it(39)+12*it(41)+2*s(14)+1*s(15)+1*s(17)+2*s(320)+1*s(325)+14
Such that:aux(55) =< 1
aux(16) =< 2
aux(53) =< 2*V
s(17) =< 2*V+1
aux(54) =< 3*V
aux(197) =< V1
s(325) =< V1+1
aux(209) =< V
it(38) =< aux(209)
it(39) =< aux(209)
it(41) =< aux(209)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(209)
it(39) =< aux(55)+aux(209)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(209)
s(14) =< s(16)
s(320) =< aux(197)
with precondition: [Out=0,V>=3,V1>=2,V>=V1]
* Chain [33,43]: 2*s(320)+6*s(322)+1*s(325)+5
Such that:aux(197) =< V1
s(325) =< V1+1
aux(214) =< V
s(320) =< aux(197)
s(322) =< aux(214)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [33,42,43]: 10*s(18)+26*s(20)+8*s(26)+2*s(320)+1*s(325)+10
Such that:aux(42) =< 1
aux(43) =< 2
aux(197) =< V1
s(325) =< V1+1
aux(218) =< V
s(20) =< aux(218)
s(26) =< aux(42)
s(18) =< aux(43)
s(320) =< aux(197)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [33,40,43]: 2*s(320)+6*s(322)+1*s(325)+14
Such that:aux(197) =< V1
s(325) =< V1+1
aux(222) =< V
s(320) =< aux(197)
s(322) =< aux(222)
with precondition: [Out=0,V1>=2,V>=V1]
* Chain [32,[38,39,41],43]: 5*it(38)+12*it(39)+22*it(41)+2*s(14)+1*s(15)+1*s(17)+10*s(329)+4*s(334)+5
Such that:aux(38) =< 1
aux(16) =< 2
aux(230) =< V
aux(232) =< V1+1
aux(36) =< 2*V1
s(17) =< 2*V1+1
aux(37) =< 3*V1
aux(234) =< V1
it(38) =< aux(234)
it(39) =< aux(234)
it(41) =< aux(234)
aux(7) =< aux(38)*3
aux(12) =< aux(38)*2
it(38) =< aux(38)+aux(234)
it(39) =< aux(38)+aux(234)
it(39) =< aux(12)+aux(36)
s(15) =< aux(12)+aux(36)
it(39) =< aux(7)+aux(37)
s(16) =< aux(7)+aux(37)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(234)
s(14) =< s(16)
s(334) =< aux(232)
s(329) =< aux(230)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [32,[38,39,41],42,43]: 5*it(38)+12*it(39)+22*it(41)+2*s(14)+1*s(15)+21*s(17)+10*s(18)+8*s(26)+10*s(329)+4*s(334)+10
Such that:aux(44) =< 2
aux(230) =< V
aux(232) =< V1+1
aux(47) =< 2*V1
aux(48) =< 2*V1+1
aux(49) =< 3*V1
aux(238) =< 1
aux(239) =< V1
s(17) =< aux(48)
s(26) =< aux(238)
s(18) =< aux(44)
it(38) =< aux(239)
it(39) =< aux(239)
it(41) =< aux(239)
aux(7) =< aux(238)*3
aux(12) =< aux(238)*2
it(38) =< aux(238)+aux(239)
it(39) =< aux(238)+aux(239)
it(39) =< aux(12)+aux(47)
s(15) =< aux(12)+aux(47)
it(39) =< aux(7)+aux(49)
s(16) =< aux(7)+aux(49)
s(15) =< it(38)*aux(44)
s(16) =< it(38)*aux(239)
s(14) =< s(16)
s(334) =< aux(232)
s(329) =< aux(230)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [32,[38,39,41],40,43]: 5*it(38)+12*it(39)+22*it(41)+2*s(14)+1*s(15)+1*s(17)+10*s(329)+4*s(334)+14
Such that:aux(55) =< 1
aux(16) =< 2
aux(230) =< V
aux(232) =< V1+1
aux(53) =< 2*V1
s(17) =< 2*V1+1
aux(54) =< 3*V1
aux(242) =< V1
it(38) =< aux(242)
it(39) =< aux(242)
it(41) =< aux(242)
aux(7) =< aux(55)*3
aux(12) =< aux(55)*2
it(38) =< aux(55)+aux(242)
it(39) =< aux(55)+aux(242)
it(39) =< aux(12)+aux(53)
s(15) =< aux(12)+aux(53)
it(39) =< aux(7)+aux(54)
s(16) =< aux(7)+aux(54)
s(15) =< it(38)*aux(16)
s(16) =< it(38)*aux(242)
s(14) =< s(16)
s(334) =< aux(232)
s(329) =< aux(230)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [32,43]: 24*s(329)+4*s(334)+2*s(343)+5
Such that:aux(231) =< V1
aux(232) =< V1+1
aux(246) =< V
s(343) =< aux(231)
s(334) =< aux(232)
s(329) =< aux(246)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [32,42,43]: 10*s(18)+44*s(20)+8*s(26)+4*s(334)+2*s(343)+10
Such that:aux(42) =< 1
aux(43) =< 2
aux(231) =< V1
aux(232) =< V1+1
aux(250) =< V
s(20) =< aux(250)
s(26) =< aux(42)
s(18) =< aux(43)
s(343) =< aux(231)
s(334) =< aux(232)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [32,40,43]: 24*s(329)+4*s(334)+2*s(343)+14
Such that:aux(231) =< V1
aux(232) =< V1+1
aux(254) =< V
s(343) =< aux(231)
s(334) =< aux(232)
s(329) =< aux(254)
with precondition: [Out=0,V>=2,V1>=2]
#### Cost of chains of start(V,V1):
* Chain [45]: 183*s(2029)+364*s(2030)+143*s(2052)+46*s(2053)+140*s(2054)+12*s(2055)+23*s(2056)+23*s(2057)+101*s(2058)+46*s(2059)+144*s(2061)+180*s(2062)+30*s(2064)+72*s(2065)+6*s(2068)+12*s(2070)+30*s(2071)+72*s(2072)+6*s(2073)+12*s(2075)+24*s(2076)+494*s(2077)+159*s(2078)+9*s(2091)+162*s(2095)+81*s(2096)+27*s(2097)+234*s(2098)+26*s(2099)+126*s(2100)+234*s(2101)+18*s(2102)+18*s(2103)+36*s(2104)+45*s(2105)+108*s(2106)+9*s(2107)+18*s(2109)+48*s(2110)+42*s(2111)+3*s(2120)+54*s(2124)+27*s(2125)+9*s(2126)+126*s(2127)+14*s(2128)+42*s(2129)+78*s(2130)+6*s(2131)+6*s(2132)+12*s(2133)+16*s(2134)+1*s(2141)+18*s(2145)+9*s(2146)+3*s(2147)+14*s(2148)+26*s(2149)+2*s(2150)+2*s(2151)+4*s(2152)+32*s(2153)+2*s(2159)+36*s(2163)+18*s(2164)+6*s(2165)+28*s(2166)+52*s(2167)+4*s(2168)+4*s(2169)+8*s(2170)+80*s(2171)+36*s(2172)+5*s(2181)+90*s(2185)+45*s(2186)+15*s(2187)+108*s(2188)+12*s(2189)+70*s(2190)+130*s(2191)+10*s(2192)+10*s(2193)+20*s(2194)+16*s(2195)+1*s(2201)+18*s(2205)+9*s(2206)+3*s(2207)+14*s(2208)+26*s(2209)+2*s(2210)+2*s(2211)+4*s(2212)+10*s(2213)+16*s(2214)+18*s(2215)+1*s(2223)+18*s(2227)+9*s(2228)+3*s(2229)+54*s(2230)+6*s(2231)+14*s(2232)+26*s(2233)+2*s(2234)+2*s(2235)+4*s(2236)+24*s(2237)+16*s(2238)+1*s(2245)+18*s(2249)+9*s(2250)+3*s(2251)+14*s(2252)+26*s(2253)+2*s(2254)+2*s(2255)+4*s(2256)+15*s(2257)+36*s(2258)+3*s(2259)+6*s(2261)+32*s(2262)+2*s(2268)+36*s(2272)+18*s(2273)+6*s(2274)+28*s(2275)+52*s(2276)+4*s(2277)+4*s(2278)+8*s(2279)+16*s(2280)+6*s(2281)+1*s(2289)+18*s(2293)+9*s(2294)+3*s(2295)+18*s(2296)+2*s(2297)+14*s(2298)+26*s(2299)+2*s(2300)+2*s(2301)+4*s(2302)+15*s(2303)+12*s(2304)+3*s(2307)+2*s(2309)+16*s(2310)+6*s(2311)+1*s(2320)+18*s(2324)+9*s(2325)+3*s(2326)+18*s(2327)+2*s(2328)+14*s(2329)+26*s(2330)+2*s(2331)+2*s(2332)+4*s(2333)+36*s(2334)+3*s(2337)+6*s(2339)+24*s(2340)+4*s(2342)+32*s(2343)+2*s(2349)+36*s(2353)+18*s(2354)+6*s(2355)+28*s(2356)+52*s(2357)+4*s(2358)+4*s(2359)+8*s(2360)+32*s(2361)+2*s(2367)+36*s(2371)+18*s(2372)+6*s(2373)+28*s(2374)+52*s(2375)+4*s(2376)+4*s(2377)+8*s(2378)+1*s(2383)+15
Such that:s(2032) =< 1
s(2033) =< 2
s(2383) =< V+2
s(2035) =< V+V1
s(2036) =< V+V1+1
s(2037) =< 2*V
s(2038) =< 2*V+1
s(2039) =< 2*V+2*V1
s(2040) =< 2*V+2*V1+1
s(2041) =< 2*V+2*V1+3
s(2042) =< 2*V+3*V1
s(2043) =< 3*V
s(2044) =< 3*V+3*V1
s(2045) =< 6*V+6*V1
s(2046) =< 9*V+9*V1
s(2048) =< V1+1
s(2049) =< 2*V1
s(2050) =< 2*V1+1
s(2051) =< 3*V1
aux(278) =< V
aux(279) =< V1
s(2030) =< aux(278)
s(2029) =< aux(279)
s(2052) =< s(2036)
s(2053) =< s(2038)
s(2054) =< s(2040)
s(2055) =< s(2041)
s(2056) =< s(2042)
s(2057) =< s(2046)
s(2058) =< s(2048)
s(2059) =< s(2050)
s(2061) =< s(2032)
s(2062) =< s(2033)
s(2064) =< aux(279)
s(2065) =< aux(279)
s(2066) =< s(2032)*3
s(2067) =< s(2032)*2
s(2064) =< s(2032)+aux(279)
s(2065) =< s(2032)+aux(279)
s(2065) =< s(2067)+s(2049)
s(2068) =< s(2067)+s(2049)
s(2065) =< s(2066)+s(2051)
s(2069) =< s(2066)+s(2051)
s(2068) =< s(2064)*s(2033)
s(2069) =< s(2064)*aux(279)
s(2070) =< s(2069)
s(2071) =< aux(278)
s(2072) =< aux(278)
s(2071) =< s(2032)+aux(278)
s(2072) =< s(2032)+aux(278)
s(2072) =< s(2067)+s(2037)
s(2073) =< s(2067)+s(2037)
s(2072) =< s(2066)+s(2043)
s(2074) =< s(2066)+s(2043)
s(2073) =< s(2071)*s(2033)
s(2074) =< s(2071)*aux(278)
s(2075) =< s(2074)
s(2076) =< s(2049)
s(2077) =< s(2035)
s(2078) =< s(2035)
s(2079) =< aux(279)
s(2080) =< aux(279)+1
s(2081) =< s(2035)
s(2082) =< s(2035)-1
s(2083) =< aux(279)*2
s(2078) =< aux(279)+aux(278)
s(2084) =< s(2077)*s(2081)
s(2085) =< s(2077)*s(2080)
s(2086) =< s(2078)*s(2079)
s(2087) =< s(2078)*s(2080)
s(2088) =< s(2078)*s(2081)
s(2089) =< s(2078)*s(2082)
s(2090) =< s(2078)*s(2083)
s(2091) =< s(2078)*s(2080)
s(2092) =< s(2078)*aux(279)
s(2093) =< s(2078)*s(2035)
s(2094) =< s(2086)*2
s(2095) =< s(2086)
s(2096) =< s(2087)
s(2097) =< s(2094)
s(2098) =< s(2084)
s(2099) =< s(2085)
s(2100) =< s(2089)
s(2101) =< s(2088)
s(2102) =< s(2092)
s(2103) =< s(2090)
s(2104) =< s(2093)
s(2105) =< s(2035)
s(2106) =< s(2035)
s(2105) =< s(2032)+s(2035)
s(2106) =< s(2032)+s(2035)
s(2106) =< s(2067)+s(2039)
s(2107) =< s(2067)+s(2039)
s(2106) =< s(2066)+s(2044)
s(2108) =< s(2066)+s(2044)
s(2107) =< s(2105)*s(2033)
s(2108) =< s(2105)*s(2035)
s(2109) =< s(2108)
s(2110) =< s(2035)
s(2111) =< s(2035)
s(2110) =< s(2040)
s(2111) =< s(2040)
s(2112) =< aux(279)
s(2112) =< s(2051)
s(2110) =< s(2112)+aux(278)
s(2113) =< s(2111)*s(2081)
s(2114) =< s(2111)*s(2080)
s(2115) =< s(2110)*s(2079)
s(2116) =< s(2110)*s(2080)
s(2117) =< s(2110)*s(2081)
s(2118) =< s(2110)*s(2082)
s(2119) =< s(2110)*s(2083)
s(2120) =< s(2110)*s(2080)
s(2121) =< s(2110)*aux(279)
s(2122) =< s(2110)*s(2035)
s(2123) =< s(2115)*2
s(2124) =< s(2115)
s(2125) =< s(2116)
s(2126) =< s(2123)
s(2127) =< s(2113)
s(2128) =< s(2114)
s(2129) =< s(2118)
s(2130) =< s(2117)
s(2131) =< s(2121)
s(2132) =< s(2119)
s(2133) =< s(2122)
s(2134) =< s(2035)
s(2135) =< aux(279)
s(2135) =< s(2050)
s(2134) =< s(2135)+aux(278)
s(2136) =< s(2134)*s(2079)
s(2137) =< s(2134)*s(2080)
s(2138) =< s(2134)*s(2081)
s(2139) =< s(2134)*s(2082)
s(2140) =< s(2134)*s(2083)
s(2141) =< s(2134)*s(2080)
s(2142) =< s(2134)*aux(279)
s(2143) =< s(2134)*s(2035)
s(2144) =< s(2136)*2
s(2145) =< s(2136)
s(2146) =< s(2137)
s(2147) =< s(2144)
s(2148) =< s(2139)
s(2149) =< s(2138)
s(2150) =< s(2142)
s(2151) =< s(2140)
s(2152) =< s(2143)
s(2153) =< s(2035)
s(2153) =< s(2040)
s(2153) =< aux(279)+aux(278)
s(2154) =< s(2153)*s(2079)
s(2155) =< s(2153)*s(2080)
s(2156) =< s(2153)*s(2081)
s(2157) =< s(2153)*s(2082)
s(2158) =< s(2153)*s(2083)
s(2159) =< s(2153)*s(2080)
s(2160) =< s(2153)*aux(279)
s(2161) =< s(2153)*s(2035)
s(2162) =< s(2154)*2
s(2163) =< s(2154)
s(2164) =< s(2155)
s(2165) =< s(2162)
s(2166) =< s(2157)
s(2167) =< s(2156)
s(2168) =< s(2160)
s(2169) =< s(2158)
s(2170) =< s(2161)
s(2171) =< s(2035)
s(2172) =< s(2035)
s(2171) =< s(2036)
s(2172) =< s(2036)
s(2173) =< aux(279)
s(2173) =< s(2048)
s(2171) =< s(2173)+aux(278)
s(2174) =< s(2172)*s(2081)
s(2175) =< s(2172)*s(2080)
s(2176) =< s(2171)*s(2079)
s(2177) =< s(2171)*s(2080)
s(2178) =< s(2171)*s(2081)
s(2179) =< s(2171)*s(2082)
s(2180) =< s(2171)*s(2083)
s(2181) =< s(2171)*s(2080)
s(2182) =< s(2171)*aux(279)
s(2183) =< s(2171)*s(2035)
s(2184) =< s(2176)*2
s(2185) =< s(2176)
s(2186) =< s(2177)
s(2187) =< s(2184)
s(2188) =< s(2174)
s(2189) =< s(2175)
s(2190) =< s(2179)
s(2191) =< s(2178)
s(2192) =< s(2182)
s(2193) =< s(2180)
s(2194) =< s(2183)
s(2195) =< s(2035)
s(2195) =< s(2112)+aux(278)
s(2196) =< s(2195)*s(2079)
s(2197) =< s(2195)*s(2080)
s(2198) =< s(2195)*s(2081)
s(2199) =< s(2195)*s(2082)
s(2200) =< s(2195)*s(2083)
s(2201) =< s(2195)*s(2080)
s(2202) =< s(2195)*aux(279)
s(2203) =< s(2195)*s(2035)
s(2204) =< s(2196)*2
s(2205) =< s(2196)
s(2206) =< s(2197)
s(2207) =< s(2204)
s(2208) =< s(2199)
s(2209) =< s(2198)
s(2210) =< s(2202)
s(2211) =< s(2200)
s(2212) =< s(2203)
s(2213) =< s(2044)
s(2214) =< s(2035)
s(2215) =< s(2035)
s(2214) =< s(2044)
s(2215) =< s(2044)
s(2214) =< s(2112)+aux(278)
s(2216) =< s(2215)*s(2081)
s(2217) =< s(2215)*s(2080)
s(2218) =< s(2214)*s(2079)
s(2219) =< s(2214)*s(2080)
s(2220) =< s(2214)*s(2081)
s(2221) =< s(2214)*s(2082)
s(2222) =< s(2214)*s(2083)
s(2223) =< s(2214)*s(2080)
s(2224) =< s(2214)*aux(279)
s(2225) =< s(2214)*s(2035)
s(2226) =< s(2218)*2
s(2227) =< s(2218)
s(2228) =< s(2219)
s(2229) =< s(2226)
s(2230) =< s(2216)
s(2231) =< s(2217)
s(2232) =< s(2221)
s(2233) =< s(2220)
s(2234) =< s(2224)
s(2235) =< s(2222)
s(2236) =< s(2225)
s(2237) =< s(2039)
s(2238) =< s(2035)
s(2238) =< s(2036)
s(2239) =< aux(279)
s(2239) =< s(2049)
s(2238) =< s(2239)+aux(278)
s(2240) =< s(2238)*s(2079)
s(2241) =< s(2238)*s(2080)
s(2242) =< s(2238)*s(2081)
s(2243) =< s(2238)*s(2082)
s(2244) =< s(2238)*s(2083)
s(2245) =< s(2238)*s(2080)
s(2246) =< s(2238)*aux(279)
s(2247) =< s(2238)*s(2035)
s(2248) =< s(2240)*2
s(2249) =< s(2240)
s(2250) =< s(2241)
s(2251) =< s(2248)
s(2252) =< s(2243)
s(2253) =< s(2242)
s(2254) =< s(2246)
s(2255) =< s(2244)
s(2256) =< s(2247)
s(2257) =< s(2039)
s(2258) =< s(2039)
s(2257) =< s(2032)+s(2039)
s(2258) =< s(2032)+s(2039)
s(2258) =< s(2067)+s(2039)
s(2259) =< s(2067)+s(2039)
s(2258) =< s(2066)+s(2045)
s(2260) =< s(2066)+s(2045)
s(2259) =< s(2257)*s(2033)
s(2260) =< s(2257)*s(2039)
s(2261) =< s(2260)
s(2262) =< s(2035)
s(2262) =< s(2040)
s(2262) =< s(2239)+aux(278)
s(2263) =< s(2262)*s(2079)
s(2264) =< s(2262)*s(2080)
s(2265) =< s(2262)*s(2081)
s(2266) =< s(2262)*s(2082)
s(2267) =< s(2262)*s(2083)
s(2268) =< s(2262)*s(2080)
s(2269) =< s(2262)*aux(279)
s(2270) =< s(2262)*s(2035)
s(2271) =< s(2263)*2
s(2272) =< s(2263)
s(2273) =< s(2264)
s(2274) =< s(2271)
s(2275) =< s(2266)
s(2276) =< s(2265)
s(2277) =< s(2269)
s(2278) =< s(2267)
s(2279) =< s(2270)
s(2280) =< s(2035)
s(2281) =< s(2035)
s(2280) =< s(2039)
s(2281) =< s(2039)
s(2280) =< s(2239)+aux(278)
s(2282) =< s(2281)*s(2081)
s(2283) =< s(2281)*s(2080)
s(2284) =< s(2280)*s(2079)
s(2285) =< s(2280)*s(2080)
s(2286) =< s(2280)*s(2081)
s(2287) =< s(2280)*s(2082)
s(2288) =< s(2280)*s(2083)
s(2289) =< s(2280)*s(2080)
s(2290) =< s(2280)*aux(279)
s(2291) =< s(2280)*s(2035)
s(2292) =< s(2284)*2
s(2293) =< s(2284)
s(2294) =< s(2285)
s(2295) =< s(2292)
s(2296) =< s(2282)
s(2297) =< s(2283)
s(2298) =< s(2287)
s(2299) =< s(2286)
s(2300) =< s(2290)
s(2301) =< s(2288)
s(2302) =< s(2291)
s(2303) =< s(2035)
s(2304) =< s(2035)
s(2305) =< s(2044)*3
s(2306) =< s(2044)*2
s(2303) =< s(2044)+s(2044)
s(2304) =< s(2044)+s(2044)
s(2304) =< s(2306)+s(2045)
s(2307) =< s(2306)+s(2045)
s(2304) =< s(2305)+s(2046)
s(2308) =< s(2305)+s(2046)
s(2307) =< s(2303)*s(2033)
s(2308) =< s(2303)*s(2035)
s(2309) =< s(2308)
s(2310) =< s(2035)
s(2311) =< s(2035)
s(2310) =< s(2046)
s(2311) =< s(2046)
s(2312) =< aux(279)
s(2312) =< s(2042)
s(2310) =< s(2312)+aux(278)
s(2313) =< s(2311)*s(2081)
s(2314) =< s(2311)*s(2080)
s(2315) =< s(2310)*s(2079)
s(2316) =< s(2310)*s(2080)
s(2317) =< s(2310)*s(2081)
s(2318) =< s(2310)*s(2082)
s(2319) =< s(2310)*s(2083)
s(2320) =< s(2310)*s(2080)
s(2321) =< s(2310)*aux(279)
s(2322) =< s(2310)*s(2035)
s(2323) =< s(2315)*2
s(2324) =< s(2315)
s(2325) =< s(2316)
s(2326) =< s(2323)
s(2327) =< s(2313)
s(2328) =< s(2314)
s(2329) =< s(2318)
s(2330) =< s(2317)
s(2331) =< s(2321)
s(2332) =< s(2319)
s(2333) =< s(2322)
s(2334) =< s(2035)
s(2335) =< aux(279)*3
s(2336) =< aux(279)*2
s(2334) =< aux(279)+aux(278)
s(2334) =< s(2336)+s(2037)
s(2337) =< s(2336)+s(2037)
s(2334) =< s(2335)+s(2043)
s(2338) =< s(2335)+s(2043)
s(2337) =< s(2078)*s(2033)
s(2338) =< s(2078)*s(2035)
s(2339) =< s(2338)
s(2340) =< s(2035)
s(2340) =< s(2044)+s(2044)
s(2340) =< s(2306)+s(2045)
s(2340) =< s(2305)+s(2044)
s(2341) =< s(2305)+s(2044)
s(2341) =< s(2303)*s(2035)
s(2342) =< s(2341)
s(2343) =< s(2035)
s(2343) =< s(2044)
s(2343) =< s(2312)+aux(278)
s(2344) =< s(2343)*s(2079)
s(2345) =< s(2343)*s(2080)
s(2346) =< s(2343)*s(2081)
s(2347) =< s(2343)*s(2082)
s(2348) =< s(2343)*s(2083)
s(2349) =< s(2343)*s(2080)
s(2350) =< s(2343)*aux(279)
s(2351) =< s(2343)*s(2035)
s(2352) =< s(2344)*2
s(2353) =< s(2344)
s(2354) =< s(2345)
s(2355) =< s(2352)
s(2356) =< s(2347)
s(2357) =< s(2346)
s(2358) =< s(2350)
s(2359) =< s(2348)
s(2360) =< s(2351)
s(2361) =< s(2035)
s(2361) =< s(2239)+aux(278)
s(2362) =< s(2361)*s(2079)
s(2363) =< s(2361)*s(2080)
s(2364) =< s(2361)*s(2081)
s(2365) =< s(2361)*s(2082)
s(2366) =< s(2361)*s(2083)
s(2367) =< s(2361)*s(2080)
s(2368) =< s(2361)*aux(279)
s(2369) =< s(2361)*s(2035)
s(2370) =< s(2362)*2
s(2371) =< s(2362)
s(2372) =< s(2363)
s(2373) =< s(2370)
s(2374) =< s(2365)
s(2375) =< s(2364)
s(2376) =< s(2368)
s(2377) =< s(2366)
s(2378) =< s(2369)
with precondition: [V>=0]
* Chain [44]: 1
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [45] with precondition: [V>=0]
- Upper bound: 466*V+711+nat(V1)*309+nat(V1)*1302*nat(V+V1)+nat(nat(V+V1)+ -1)*434*nat(V+V1)+18*V+nat(2*V1)*30+54*V+nat(3*V1)*12+nat(V+V1)*1725+nat(V+V1)*1488*nat(V+V1)+ (V+2)+nat(V1+1)*101+ (92*V+46)+nat(2*V+2*V1)*87+nat(2*V+3*V1)*23+nat(2*V1+1)*46+nat(3*V+3*V1)*56+nat(6*V+6*V1)*9+nat(9*V+9*V1)*25+nat(V+V1+1)*143+nat(2*V+2*V1+1)*140+nat(2*V+2*V1+3)*12
- Complexity: n^2
* Chain [44] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
### Maximum cost of start(V,V1): 466*V+710+nat(V1)*309+nat(V1)*1302*nat(V+V1)+nat(nat(V+V1)+ -1)*434*nat(V+V1)+18*V+nat(2*V1)*30+54*V+nat(3*V1)*12+nat(V+V1)*1725+nat(V+V1)*1488*nat(V+V1)+ (V+2)+nat(V1+1)*101+ (92*V+46)+nat(2*V+2*V1)*87+nat(2*V+3*V1)*23+nat(2*V1+1)*46+nat(3*V+3*V1)*56+nat(6*V+6*V1)*9+nat(9*V+9*V1)*25+nat(V+V1+1)*143+nat(2*V+2*V1+1)*140+nat(2*V+2*V1+3)*12+1
Asymptotic class: n^2
* Total analysis performed in 12162 ms.